<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Meet the community</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  

  <div class="row mt-5">
    <div class="col">
        <h1 id="meet-the-community" class="markdown-heading">Meet the community <a class="hover-link" href="#meet-the-community">#</a></h1>
<p>The Lean community is rather diverse. We have users coming from computer
science as well as mathematics, and even a couple of people with a
physics background.
Most users are either students or work in academia, but there also some
data scientists and software engineers working in industry.</p>
<h2 id="the-lean-zulip-chat" class="markdown-heading">The Lean Zulip chat <a class="hover-link" href="#the-lean-zulip-chat">#</a></h2>
<p>The main gathering point of our community is a
<a href="https://leanprover.zulipchat.com">Zulip chat instance</a>.
Since this chatroom is only visible to registered users, we provide an
<a href="https://leanprover-community.github.io/archive/">openly accessible archive</a>
of the public discussions.
This is useful for quick reference; for a better browsing interface,
and to participate in the discussions, we strongly suggest joining the chat.
Registering with your real name is preferred, but not required.
Starting by briefly introducing youself is also appreciated.</p>
<p>Questions from users at all levels of expertise are welcomed.
Asking your first questions in the <em>new members</em> stream will ensure the answers
won't asssume you know much about Lean. But you are welcome to use more specialized streams.
Please start new discussion topics rather than using unrelated existing topics.
If you need coding help, you may be asked to provide a <a href="mwe.html">MWE</a>.
Also beware of <a href="https://mywiki.wooledge.org/XyProblem">XY problems</a>: try to give enough context.</p>
<p>To post a snippet of code inline, enclose it in single backticks: <code>`my code here`</code>.
If your code contains backticks itself, enclose it in more backticks than it contains:
<code>`` my`code`contains`backticks ``</code>.</p>
<p>Longer snippets should be enclosed between two lines containing three back-quotes, as in:</p>
<pre><code>```
def my_nat : n := 5
#check my_nat
```
</code></pre>
<p>You can use LaTeX using <code>$$</code> to enclose inline LaTeX and</p>
<pre><code>```latex
my LaTeX code here
```
</code></pre>
<p>for displayed math.</p>
<h2 id="github" class="markdown-heading">GitHub <a class="hover-link" href="#github">#</a></h2>
<p>The next gathering point after Zulip is GitHub, which hosts all the
<a href="https://github.com/leanprover-community">community repositories</a>.
In particular, the
<a href="https://github.com/leanprover-community/mathlib/pulls">mathlib pull requests</a>
page is the right place to see our ongoing efforts.</p>
<p>If you want to participate in our projects then you can read our
<a href="contribute/index.html">contributing guide</a>.</p>
<h2 id="workshops-and-conferences" class="markdown-heading">Workshops and conferences <a class="hover-link" href="#workshops-and-conferences">#</a></h2>
<p>In addition to general formal methods conferences such as CPP and ITP,
the Lean community gathers at specific events.
The largest past events were:</p>
<ul>
<li><a href="http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/">FoMM 2020</a></li>
<li><a href="https://lean-forward.github.io/lean-together/2019/">Lean Together 2019</a></li>
</ul>

    </div>
  </div>

  <div class="row mt-3">
    <div class="col">
        <a name="maintainers"></a> 
        <h2>Mathlib maintainers</h2>
        
        Mathlib maintainers are community members who are actively
		developing mathlib and reviewing pull requests.
		Their number grows naturally when new users become
		frequent contributors.

  <div class="row mt-3">
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/jeremy.png" class="p-2" 
													  alt="Jeremy Avigad
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Jeremy Avigad</h5>
					<p class="card-text">Jeremy is a Professor of Philosophy at Carnegie Mellon University
(USA).  He did a PhD in mathematical logic at Berkeley, and has
been formalizing mathematics since 2002, in Isabelle, Coq and
Lean.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/anne.jpg" class="p-2" 
													  alt="Anne Baanen
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Anne Baanen</h5>
					<p class="card-text">Anne is a PhD student at Vrije Universiteit Amsterdam (The Netherlands).
They have been formalizing proofs in mathematics and computer science
since 2018.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/reid.jpg" class="p-2" 
													  alt="Reid Barton
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Reid Barton</h5>
					<p class="card-text">Reid is a post-doc at the University of Pittsburgh (USA). He did a PhD
in algebraic topology in Harvard. He worked on the Glasgow
Haskell Compiler, and has been formalizing mathematics since
2017.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/mario.jpg" class="p-2" 
													  alt="Mario Carneiro
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Mario Carneiro</h5>
					<p class="card-text">Mario is a PhD student at Carnegie Mellon University (USA). He
has been formalizing mathematics since 2013, first in metamath
and then in Lean.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/bryan.jpg" class="p-2" 
													  alt="Bryan Gin-ge Chen
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Bryan Gin-ge Chen</h5>
					<p class="card-text">Bryan is a data-scientist in Dayton (USA). He did a PhD in
theoretical condensed matter physics at University of
Pennsylvania. He has been formalizing mathematics and helping
with the community infrastructure since 2018.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/Johan.jpg" class="p-2" 
													  alt="Johan Commelin
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Johan Commelin</h5>
					<p class="card-text">Johan is a post-doc at Universität Freiburg (Germany).  He did a
PhD in algebraic geometry in Nijmegen.  He has been formalizing
mathematics since 2018.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/floris.jpeg" class="p-2" 
													  alt="Floris van Doorn
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Floris van Doorn</h5>
					<p class="card-text">Floris is a post-doc at the University of Pittsburgh (USA).  He did a
PhD in formalized mathematics and type theory in Pittsburgh.  He
has been formalizing mathematics since 2013.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/gabriel.jpeg" class="p-2" 
													  alt="Gabriel Ebner
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Gabriel Ebner</h5>
					<p class="card-text">Gabriel is a post-doc at Vrije Universiteit Amsterdam
(The Netherlands).  He did a PhD in computational proof theory at
TU Wien (Austria).  He developed the current parallel compilation
infrastructure and interactive editor integration for Lean, and
has been formalizing mathematics since 2016.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/sebastien.jpg" class="p-2" 
													  alt="Sébastien Gouëzel
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Sébastien Gouëzel</h5>
					<p class="card-text">Sébastien is a Professor of Mathematics at Université de Nantes
(France).  He did a PhD in dynamical systems in Orsay.  He has
been formalizing mathematics since 2016, first in Isabelle and
now in Lean.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/Simon.jpg" class="p-2" 
													  alt="Simon Hudon
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Simon Hudon</h5>
					<p class="card-text">Simon is a post-doc at Carnegie Mellon University (USA).  He did
a PhD in computer science in Toronto.  He has been writing Lean
tactics since 2017.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/chris.png" class="p-2" 
													  alt="Chris Hughes
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Chris Hughes</h5>
					<p class="card-text">Chris is an undergrad student in mathematics at Imperial College
London (UK).  He has been formalizing mathematics since 2017.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/yury.jpeg" class="p-2" 
													  alt="Yury G. Kudryashov
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Yury G. Kudryashov</h5>
					<p class="card-text">Yury is a post-doc in mathematics at the Univerity of Toronto
(Canada).  He did a PhD in dynamical systems in Lyon and Moscow.
He has been formalizing mathematics since 2019.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/rob.png" class="p-2" 
													  alt="Robert Y. Lewis
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Robert Y. Lewis</h5>
					<p class="card-text">Rob is a post-doc at Vrije Universiteit Amsterdam (Netherlands).
He did a PhD in Pure and Applied Logic at Carnegie Mellon
University in Pittsburgh. He has been formalizing mathematics
since 2014.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/patrick.png" class="p-2" 
													  alt="Patrick Massot
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Patrick Massot</h5>
					<p class="card-text">Patrick is a Professor of Mathematics at Université Paris-Saclay
at Orsay (France).  He did a PhD in differential topology in
Lyon.  He has been formalizing mathematics since 2017.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		<div class="col-md-6">
			<div class="card mb-3">
			  <div class="row no-gutters">
				<div class="col-md-3 d-flex align-items-center justify-content-center">
				  <img src="img/Scott.jpg" class="p-2" 
													  alt="Scott Morrison
													  picture">
				</div>
				<div class="col-md-9">
				  <div class="card-body">
					<h5 class="card-title">Scott Morrison</h5>
					<p class="card-text">Scott is an Associate Professor of Mathematics at the Australian
National Univerity (Australia).  He did a PhD in topology and
category theory in Berkeley.  He has been formalizing mathematics
since 2017.
</p>
				  </div>
				</div>
			  </div>
			</div>
		</div>
        
		</div>
    </div>
  </div>


  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>